(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_NRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(assert (let ((e2 7))
(let ((e3 1))
(let ((e4 0))
(let ((e5 (* v1 v1)))
(let ((e6 (+ v1 e5)))
(let ((e7 (+ v1 e6)))
(let ((e8 (* e5 e7)))
(let ((e9 (+ v1 e8)))
(let ((e10 (- e5)))
(let ((e11 (- e6 e5)))
(let ((e12 (+ e6 e11)))
(let ((e13 (/ e3 (- e2))))
(let ((e14 (* e10 e8)))
(let ((e15 (+ e14 e9)))
(let ((e16 (- e6 e12)))
(let ((e17 (- e9 e8)))
(let ((e18 (* e7 e16)))
(let ((e19 (+ e8 e13)))
(let ((e20 (- e13)))
(let ((e21 (- e19 e12)))
(let ((e22 (* e13 e12)))
(let ((e23 (+ e10 e17)))
(let ((e24 (- e19 e7)))
(let ((e25 (- v0)))
(let ((e26 (- v0 e20)))
(let ((e27 (- e8 e17)))
(let ((e28 (- e7)))
(let ((e29 (- e27)))
(let ((e30 (- e18 e9)))
(let ((e31 (- e6 e21)))
(let ((e32 (+ e25 e16)))
(let ((e33 (/ e4 e3)))
(let ((e34 (distinct v0 e19)))
(let ((e35 (< e18 e5)))
(let ((e36 (<= e21 e16)))
(let ((e37 (distinct e19 e5)))
(let ((e38 (= e23 e27)))
(let ((e39 (= e5 e15)))
(let ((e40 (> e25 e7)))
(let ((e41 (distinct e25 e29)))
(let ((e42 (<= e14 e12)))
(let ((e43 (< e33 e29)))
(let ((e44 (>= e15 e19)))
(let ((e45 (< e20 e30)))
(let ((e46 (distinct e27 e31)))
(let ((e47 (= e28 e33)))
(let ((e48 (>= e20 e17)))
(let ((e49 (= v1 e10)))
(let ((e50 (< e6 e19)))
(let ((e51 (<= e23 e22)))
(let ((e52 (distinct e26 e31)))
(let ((e53 (= e20 e18)))
(let ((e54 (distinct e19 e28)))
(let ((e55 (<= e5 e19)))
(let ((e56 (>= e12 v0)))
(let ((e57 (<= e28 e29)))
(let ((e58 (< e17 e13)))
(let ((e59 (<= e27 e30)))
(let ((e60 (> e32 e19)))
(let ((e61 (= e12 e26)))
(let ((e62 (>= e5 e25)))
(let ((e63 (< e5 e11)))
(let ((e64 (distinct e14 e32)))
(let ((e65 (< e30 e18)))
(let ((e66 (> e30 e7)))
(let ((e67 (< v1 e16)))
(let ((e68 (distinct e18 e16)))
(let ((e69 (= e14 e19)))
(let ((e70 (< v1 e13)))
(let ((e71 (<= e22 e23)))
(let ((e72 (> e12 e20)))
(let ((e73 (= e9 e22)))
(let ((e74 (< e13 e11)))
(let ((e75 (< e32 v1)))
(let ((e76 (= e19 e9)))
(let ((e77 (= e24 e17)))
(let ((e78 (>= e30 e15)))
(let ((e79 (>= e11 e6)))
(let ((e80 (< e27 e13)))
(let ((e81 (distinct e18 e23)))
(let ((e82 (= e7 e9)))
(let ((e83 (>= e27 e16)))
(let ((e84 (distinct e12 e31)))
(let ((e85 (distinct e29 e6)))
(let ((e86 (< v1 e10)))
(let ((e87 (< e32 e32)))
(let ((e88 (= e18 e31)))
(let ((e89 (< e11 e26)))
(let ((e90 (> e28 e8)))
(let ((e91 (= e18 e14)))
(let ((e92 (< e25 v1)))
(let ((e93 (> e8 v0)))
(let ((e94 (= v1 e20)))
(let ((e95 (= e21 e32)))
(let ((e96 (>= e29 e21)))
(let ((e97 (distinct e23 e6)))
(let ((e98 (>= e27 e7)))
(let ((e99 (> e14 e26)))
(let ((e100 (<= e14 e32)))
(let ((e101 (= e6 e21)))
(let ((e102 (= e20 e13)))
(let ((e103 (distinct e25 e6)))
(let ((e104 (distinct e17 e15)))
(let ((e105 (= e27 e17)))
(let ((e106 (= e10 e25)))
(let ((e107 (distinct e17 e23)))
(let ((e108 (>= e24 e15)))
(let ((e109 (<= e23 e6)))
(let ((e110 (< e20 e31)))
(let ((e111 (distinct v1 e12)))
(let ((e112 (distinct e8 e11)))
(let ((e113 (< e11 e7)))
(let ((e114 (<= e20 e23)))
(let ((e115 (>= e16 v1)))
(let ((e116 (> e26 e26)))
(let ((e117 (<= v0 e6)))
(let ((e118 (<= e21 e17)))
(let ((e119 (<= e24 e10)))
(let ((e120 (>= v0 e21)))
(let ((e121 (< e7 e14)))
(let ((e122 (<= e33 e6)))
(let ((e123 (>= e22 e23)))
(let ((e124 (= e14 e13)))
(let ((e125 (< e6 e33)))
(let ((e126 (< e33 e5)))
(let ((e127 (>= e5 e8)))
(let ((e128 (< v1 e25)))
(let ((e129 (>= e27 e7)))
(let ((e130 (>= v0 e26)))
(let ((e131 (> e29 e12)))
(let ((e132 (< e5 e10)))
(let ((e133 (< e11 e13)))
(let ((e134 (< e14 e19)))
(let ((e135 (< e9 e10)))
(let ((e136 (distinct e31 v1)))
(let ((e137 (= e28 v0)))
(let ((e138 (<= e24 e15)))
(let ((e139 (<= e15 e29)))
(let ((e140 (> e23 e22)))
(let ((e141 (= e15 v1)))
(let ((e142 (< e9 e10)))
(let ((e143 (<= e15 e16)))
(let ((e144 (< e20 v1)))
(let ((e145 (>= e16 e15)))
(let ((e146 (= v0 v0)))
(let ((e147 (= e31 e12)))
(let ((e148 (< e32 e21)))
(let ((e149 (> v1 e8)))
(let ((e150 (= e26 e15)))
(let ((e151 (> e11 e16)))
(let ((e152 (< e20 e21)))
(let ((e153 (>= e24 v0)))
(let ((e154 (>= e13 e19)))
(let ((e155 (> e32 e23)))
(let ((e156 (= e33 e29)))
(let ((e157 (<= e21 e32)))
(let ((e158 (distinct e11 e32)))
(let ((e159 (distinct e15 e20)))
(let ((e160 (>= e5 e15)))
(let ((e161 (distinct e18 e31)))
(let ((e162 (distinct v0 e14)))
(let ((e163 (= e22 e19)))
(let ((e164 (>= e18 e29)))
(let ((e165 (> v0 e11)))
(let ((e166 (>= e11 e15)))
(let ((e167 (>= e19 e28)))
(let ((e168 (< e19 e16)))
(let ((e169 (< e8 e15)))
(let ((e170 (> e24 e7)))
(let ((e171 (<= e18 e32)))
(let ((e172 (> e25 e19)))
(let ((e173 (>= e29 e26)))
(let ((e174 (> e27 e9)))
(let ((e175 (< e6 e27)))
(let ((e176 (<= e25 e22)))
(let ((e177 (distinct e30 e8)))
(let ((e178 (not e35)))
(let ((e179 (=> e131 e94)))
(let ((e180 (and e142 e56)))
(let ((e181 (or e154 e124)))
(let ((e182 (= e96 e69)))
(let ((e183 (or e107 e128)))
(let ((e184 (=> e134 e64)))
(let ((e185 (and e129 e158)))
(let ((e186 (xor e81 e162)))
(let ((e187 (=> e42 e135)))
(let ((e188 (ite e182 e106 e77)))
(let ((e189 (=> e168 e164)))
(let ((e190 (=> e115 e185)))
(let ((e191 (ite e52 e159 e179)))
(let ((e192 (xor e71 e139)))
(let ((e193 (= e156 e58)))
(let ((e194 (xor e83 e36)))
(let ((e195 (or e183 e89)))
(let ((e196 (=> e165 e34)))
(let ((e197 (xor e122 e75)))
(let ((e198 (= e53 e127)))
(let ((e199 (not e82)))
(let ((e200 (= e169 e190)))
(let ((e201 (not e126)))
(let ((e202 (and e72 e44)))
(let ((e203 (=> e141 e189)))
(let ((e204 (=> e199 e48)))
(let ((e205 (and e194 e123)))
(let ((e206 (ite e201 e188 e45)))
(let ((e207 (and e186 e114)))
(let ((e208 (xor e51 e161)))
(let ((e209 (not e79)))
(let ((e210 (ite e61 e176 e57)))
(let ((e211 (ite e97 e120 e208)))
(let ((e212 (ite e38 e108 e175)))
(let ((e213 (=> e206 e86)))
(let ((e214 (ite e73 e41 e197)))
(let ((e215 (xor e133 e87)))
(let ((e216 (ite e209 e80 e109)))
(let ((e217 (=> e99 e155)))
(let ((e218 (or e63 e136)))
(let ((e219 (ite e187 e93 e171)))
(let ((e220 (not e119)))
(let ((e221 (and e46 e178)))
(let ((e222 (=> e210 e166)))
(let ((e223 (ite e220 e191 e91)))
(let ((e224 (not e222)))
(let ((e225 (=> e116 e68)))
(let ((e226 (ite e78 e40 e140)))
(let ((e227 (and e214 e192)))
(let ((e228 (not e180)))
(let ((e229 (ite e54 e200 e101)))
(let ((e230 (not e167)))
(let ((e231 (or e67 e132)))
(let ((e232 (and e226 e147)))
(let ((e233 (ite e203 e231 e144)))
(let ((e234 (not e49)))
(let ((e235 (xor e232 e65)))
(let ((e236 (or e70 e74)))
(let ((e237 (or e193 e224)))
(let ((e238 (and e172 e174)))
(let ((e239 (or e76 e104)))
(let ((e240 (ite e47 e95 e130)))
(let ((e241 (= e60 e205)))
(let ((e242 (=> e236 e202)))
(let ((e243 (ite e110 e213 e177)))
(let ((e244 (= e152 e242)))
(let ((e245 (or e92 e217)))
(let ((e246 (and e100 e121)))
(let ((e247 (xor e216 e215)))
(let ((e248 (=> e207 e234)))
(let ((e249 (not e223)))
(let ((e250 (or e238 e240)))
(let ((e251 (xor e145 e146)))
(let ((e252 (not e59)))
(let ((e253 (and e227 e184)))
(let ((e254 (ite e149 e241 e218)))
(let ((e255 (or e250 e163)))
(let ((e256 (= e246 e118)))
(let ((e257 (=> e211 e221)))
(let ((e258 (not e85)))
(let ((e259 (and e125 e160)))
(let ((e260 (= e229 e229)))
(let ((e261 (ite e112 e228 e204)))
(let ((e262 (xor e252 e84)))
(let ((e263 (xor e251 e90)))
(let ((e264 (=> e196 e55)))
(let ((e265 (=> e230 e151)))
(let ((e266 (not e249)))
(let ((e267 (and e219 e225)))
(let ((e268 (not e257)))
(let ((e269 (= e248 e43)))
(let ((e270 (=> e153 e198)))
(let ((e271 (or e235 e148)))
(let ((e272 (xor e264 e102)))
(let ((e273 (= e268 e88)))
(let ((e274 (= e66 e212)))
(let ((e275 (and e237 e150)))
(let ((e276 (not e258)))
(let ((e277 (xor e273 e170)))
(let ((e278 (xor e244 e272)))
(let ((e279 (= e262 e239)))
(let ((e280 (=> e266 e269)))
(let ((e281 (ite e113 e278 e105)))
(let ((e282 (not e263)))
(let ((e283 (not e173)))
(let ((e284 (or e259 e256)))
(let ((e285 (=> e181 e279)))
(let ((e286 (xor e103 e137)))
(let ((e287 (or e247 e37)))
(let ((e288 (= e62 e277)))
(let ((e289 (ite e243 e138 e276)))
(let ((e290 (= e280 e233)))
(let ((e291 (=> e143 e39)))
(let ((e292 (=> e111 e261)))
(let ((e293 (ite e291 e270 e270)))
(let ((e294 (=> e283 e265)))
(let ((e295 (and e285 e254)))
(let ((e296 (=> e295 e293)))
(let ((e297 (ite e296 e287 e287)))
(let ((e298 (and e284 e297)))
(let ((e299 (and e281 e245)))
(let ((e300 (xor e98 e117)))
(let ((e301 (xor e274 e275)))
(let ((e302 (ite e286 e267 e255)))
(let ((e303 (ite e294 e301 e301)))
(let ((e304 (or e282 e157)))
(let ((e305 (ite e195 e292 e299)))
(let ((e306 (not e289)))
(let ((e307 (not e253)))
(let ((e308 (= e304 e306)))
(let ((e309 (=> e290 e260)))
(let ((e310 (and e302 e302)))
(let ((e311 (ite e305 e308 e271)))
(let ((e312 (= e311 e307)))
(let ((e313 (xor e309 e312)))
(let ((e314 (and e303 e288)))
(let ((e315 (not e300)))
(let ((e316 (not e315)))
(let ((e317 (xor e50 e298)))
(let ((e318 (= e316 e317)))
(let ((e319 (=> e310 e313)))
(let ((e320 (not e318)))
(let ((e321 (or e320 e319)))
(let ((e322 (= e314 e314)))
(let ((e323 (= e322 e322)))
(let ((e324 (xor e323 e323)))
(let ((e325 (= e324 e321)))
e325
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
